FDL - Nuprl Lemma : Q-R-pre-preserving-1-1

Nuprl Lemma : Q-R-pre-preserving-1-1

es:ES, P:(E

), Q, R:(E

E

), f:({e:E| P(e)}

E).
Refl(E;e,e'.Q(e,e'))

AntiSym(E;e,e'.R(e,e'))

f is Q-R-pre-preserving on P

Inj({e:E| P(e)} ;E;f)

Definitions ES, t T, Type, , x:A. B(x), E, x:AB(x), f(a), {x:A| B(x)} , s = t, P Q, <a, b>, Inj(A;B;f), f is Q-R-pre-preserving on P, AntiSym(T;x,y.R(x;y)), Refl(T;x,y.E(x;y)), P & Q, s ~ t, {T}, SQType(T), let x,y = A in B(x;y), t.1, x:A B(x), b, A c B

Lemmas es-E wf, event system wf